|
| 1: |
|
app(app(eq,0),0) |
→ true |
| 2: |
|
app(app(eq,0),app(s,x)) |
→ false |
| 3: |
|
app(app(eq,app(s,x)),0) |
→ false |
| 4: |
|
app(app(eq,app(s,x)),app(s,y)) |
→ app(app(eq,x),y) |
| 5: |
|
app(app(or,true),y) |
→ true |
| 6: |
|
app(app(or,false),y) |
→ y |
| 7: |
|
app(app(union,empty),h) |
→ h |
| 8: |
|
app(app(union,app(app(app(edge,x),y),i)),h) |
→ app(app(app(edge,x),y),app(app(union,i),h)) |
| 9: |
|
app(app(app(app(reach,x),y),empty),h) |
→ false |
| 10: |
|
app(app(app(app(reach,x),y),app(app(app(edge,u),v),i)),h) |
→ app(app(app(app(app(if_reach_1,app(app(eq,x),u)),x),y),app(app(app(edge,u),v),i)),h) |
| 11: |
|
app(app(app(app(app(if_reach_1,true),x),y),app(app(app(edge,u),v),i)),h) |
→ app(app(app(app(app(if_reach_2,app(app(eq,y),v)),x),y),app(app(app(edge,u),v),i)),h) |
| 12: |
|
app(app(app(app(app(if_reach_1,false),x),y),app(app(app(edge,u),v),i)),h) |
→ app(app(app(app(reach,x),y),i),app(app(app(edge,u),v),h)) |
| 13: |
|
app(app(app(app(app(if_reach_2,true),x),y),app(app(app(edge,u),v),i)),h) |
→ true |
| 14: |
|
app(app(app(app(app(if_reach_2,false),x),y),app(app(app(edge,u),v),i)),h) |
→ app(app(or,app(app(app(app(reach,x),y),i),h)),app(app(app(app(reach,v),y),app(app(union,i),h)),empty)) |
|
There are 36 dependency pairs:
|
| 15: |
|
APP(app(eq,app(s,x)),app(s,y)) |
→ APP(app(eq,x),y) |
| 16: |
|
APP(app(eq,app(s,x)),app(s,y)) |
→ APP(eq,x) |
| 17: |
|
APP(app(union,app(app(app(edge,x),y),i)),h) |
→ APP(app(app(edge,x),y),app(app(union,i),h)) |
| 18: |
|
APP(app(union,app(app(app(edge,x),y),i)),h) |
→ APP(app(union,i),h) |
| 19: |
|
APP(app(union,app(app(app(edge,x),y),i)),h) |
→ APP(union,i) |
| 20: |
|
APP(app(app(app(reach,x),y),app(app(app(edge,u),v),i)),h) |
→ APP(app(app(app(app(if_reach_1,app(app(eq,x),u)),x),y),app(app(app(edge,u),v),i)),h) |
| 21: |
|
APP(app(app(app(reach,x),y),app(app(app(edge,u),v),i)),h) |
→ APP(app(app(app(if_reach_1,app(app(eq,x),u)),x),y),app(app(app(edge,u),v),i)) |
| 22: |
|
APP(app(app(app(reach,x),y),app(app(app(edge,u),v),i)),h) |
→ APP(app(app(if_reach_1,app(app(eq,x),u)),x),y) |
| 23: |
|
APP(app(app(app(reach,x),y),app(app(app(edge,u),v),i)),h) |
→ APP(app(if_reach_1,app(app(eq,x),u)),x) |
| 24: |
|
APP(app(app(app(reach,x),y),app(app(app(edge,u),v),i)),h) |
→ APP(if_reach_1,app(app(eq,x),u)) |
| 25: |
|
APP(app(app(app(reach,x),y),app(app(app(edge,u),v),i)),h) |
→ APP(app(eq,x),u) |
| 26: |
|
APP(app(app(app(reach,x),y),app(app(app(edge,u),v),i)),h) |
→ APP(eq,x) |
| 27: |
|
APP(app(app(app(app(if_reach_1,true),x),y),app(app(app(edge,u),v),i)),h) |
→ APP(app(app(app(app(if_reach_2,app(app(eq,y),v)),x),y),app(app(app(edge,u),v),i)),h) |
| 28: |
|
APP(app(app(app(app(if_reach_1,true),x),y),app(app(app(edge,u),v),i)),h) |
→ APP(app(app(app(if_reach_2,app(app(eq,y),v)),x),y),app(app(app(edge,u),v),i)) |
| 29: |
|
APP(app(app(app(app(if_reach_1,true),x),y),app(app(app(edge,u),v),i)),h) |
→ APP(app(app(if_reach_2,app(app(eq,y),v)),x),y) |
| 30: |
|
APP(app(app(app(app(if_reach_1,true),x),y),app(app(app(edge,u),v),i)),h) |
→ APP(app(if_reach_2,app(app(eq,y),v)),x) |
| 31: |
|
APP(app(app(app(app(if_reach_1,true),x),y),app(app(app(edge,u),v),i)),h) |
→ APP(if_reach_2,app(app(eq,y),v)) |
| 32: |
|
APP(app(app(app(app(if_reach_1,true),x),y),app(app(app(edge,u),v),i)),h) |
→ APP(app(eq,y),v) |
| 33: |
|
APP(app(app(app(app(if_reach_1,true),x),y),app(app(app(edge,u),v),i)),h) |
→ APP(eq,y) |
| 34: |
|
APP(app(app(app(app(if_reach_1,false),x),y),app(app(app(edge,u),v),i)),h) |
→ APP(app(app(app(reach,x),y),i),app(app(app(edge,u),v),h)) |
| 35: |
|
APP(app(app(app(app(if_reach_1,false),x),y),app(app(app(edge,u),v),i)),h) |
→ APP(app(app(reach,x),y),i) |
| 36: |
|
APP(app(app(app(app(if_reach_1,false),x),y),app(app(app(edge,u),v),i)),h) |
→ APP(app(reach,x),y) |
| 37: |
|
APP(app(app(app(app(if_reach_1,false),x),y),app(app(app(edge,u),v),i)),h) |
→ APP(reach,x) |
| 38: |
|
APP(app(app(app(app(if_reach_1,false),x),y),app(app(app(edge,u),v),i)),h) |
→ APP(app(app(edge,u),v),h) |
| 39: |
|
APP(app(app(app(app(if_reach_2,false),x),y),app(app(app(edge,u),v),i)),h) |
→ APP(app(or,app(app(app(app(reach,x),y),i),h)),app(app(app(app(reach,v),y),app(app(union,i),h)),empty)) |
| 40: |
|
APP(app(app(app(app(if_reach_2,false),x),y),app(app(app(edge,u),v),i)),h) |
→ APP(or,app(app(app(app(reach,x),y),i),h)) |
| 41: |
|
APP(app(app(app(app(if_reach_2,false),x),y),app(app(app(edge,u),v),i)),h) |
→ APP(app(app(app(reach,x),y),i),h) |
| 42: |
|
APP(app(app(app(app(if_reach_2,false),x),y),app(app(app(edge,u),v),i)),h) |
→ APP(app(app(reach,x),y),i) |
| 43: |
|
APP(app(app(app(app(if_reach_2,false),x),y),app(app(app(edge,u),v),i)),h) |
→ APP(app(reach,x),y) |
| 44: |
|
APP(app(app(app(app(if_reach_2,false),x),y),app(app(app(edge,u),v),i)),h) |
→ APP(reach,x) |
| 45: |
|
APP(app(app(app(app(if_reach_2,false),x),y),app(app(app(edge,u),v),i)),h) |
→ APP(app(app(app(reach,v),y),app(app(union,i),h)),empty) |
| 46: |
|
APP(app(app(app(app(if_reach_2,false),x),y),app(app(app(edge,u),v),i)),h) |
→ APP(app(app(reach,v),y),app(app(union,i),h)) |
| 47: |
|
APP(app(app(app(app(if_reach_2,false),x),y),app(app(app(edge,u),v),i)),h) |
→ APP(app(reach,v),y) |
| 48: |
|
APP(app(app(app(app(if_reach_2,false),x),y),app(app(app(edge,u),v),i)),h) |
→ APP(reach,v) |
| 49: |
|
APP(app(app(app(app(if_reach_2,false),x),y),app(app(app(edge,u),v),i)),h) |
→ APP(app(union,i),h) |
| 50: |
|
APP(app(app(app(app(if_reach_2,false),x),y),app(app(app(edge,u),v),i)),h) |
→ APP(union,i) |
|
The approximated dependency graph contains one SCC:
{15,18,20-23,25,27-30,32,34-36,39,41-43,45-47,49}.